T:Type, as:(T List), bs:(Top List), P:({x:T| (x  as)} ), f:Top.
mapfilter(f;P;as @ bs) ~ (mapfilter(f;P;as) @ mapfilter(f;P;bs)) 

latex

Definitions

s = t, t  T, , Type, type List, A List, x:AB(x), x:A. B(x), [car / cdr], (x  l), , {x:A| B(x)} , s ~ t, Top, [], mapfilter(f;P;L), b, A, ff, f(a), b, P  Q, x:A  B(x), P & Q, P  Q, p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, x f y, a < b, [d], p  q, p  q, p q, tt, , Unit, left + right, hd(l), l[i], A  B, a < b, x:A.B(x), filter(P;l), map(f;as), as @ bs, #$n, ||as||, n+m, i  j , i  j < k, {i..j}, Void, False, , |g|, S  T, A c B, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , {T}, P  Q, P  Q, last(L), x:A. B(x), x. t(x), suptype(S; T)

Lemmas

subtype rel function, subtype rel set, cons member, select wf, select member, nat wf, int seg wf, non neg length, length wf1, le wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, member wf, subtype rel wf, bnot wf, not wf, assert wf, top wf, l member wf, bool wf